package com.graphcoloring;

import java.util.List;

import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ISolver;

public class OrderEncodingSolver implements Solver {
	@Override
	public Solution solve(GraphInputData data) throws Exception {
		int n = data.getVertexNumber();
        List<Integer[]> edges = data.getEdgeList();

        int colorCount = n;
        int colors[] = new int[n];
        for (int k = n; k >= 1; k--) {
            ISolver solver = SolverFactory.newDefault();
            solver.setTimeout(60);
            solver.newVar(n * k);

            for (Integer[] edge : edges) {
                int vertex1 = edge[0] + 1;
                int vertex2 = edge[1] + 1;

                for (int j = 0; j < k; j++) {
                	if (j == 0) {
	                    int clause[] = {-(vertex1 * k - j), -(vertex2 * k - j)};
	                    solver.addClause(new VecInt(clause));
                	} 
                	else {                		
                		int clause1[] = {-(vertex1 * k - j), -(vertex2 * k - j), vertex1 * k - j + 1, vertex2 * k - j + 1};
	                    solver.addClause(new VecInt(clause1));
                	}
                }
            }
            
            for (int i = 0; i < n; i++) {
            	solver.addClause(new VecInt(new int[] { k*i + 1 }));
                
                for (int j = 1; j < k; j++) {
                	int clause[] = new int[2];
                    clause[0] = k*i+j;
                    clause[1] = -(k*i+j+1);
                    solver.addClause(new VecInt(clause));
                }
            }
            if (solver.isSatisfiable()) {
                colorCount = k;
                
                for (int t = 0; t < n; t++) colors[t] = -1;

                int[] model = solver.model();
                for (int var : model) {
                    if (var > 0) {
                        int vertex = (var - 1) / k;
                        int color = (var - 1 + k) % k;
                        
                        if (color > colors[vertex]) 
                        	colors[vertex] = color;
                    }
                }
            } else {
                Solution solution = new Solution();
                solution.colorCount = colorCount;
                solution.colors = colors;

                return solution;
            }

        }
        return null;
	}
}
